Nuprl Definition : d-machine 11,40

d-machine(i;M;dec)
== <dec
== k,v,s,x. if islocal(kdestination(lnk(k)) = i
== then M.ef(k,x,read-state(s),v)?s(x)
== else s(x)
== fi 
== k,v,s. if islocal(kdestination(lnk(k)) = i
== then filter(m.source(mlnk(m)) = i;M.sends(k,s,v))
== else []
== fi > 
latex


Definitions<ab>, M.ef(k,x,s,v)?w, read-state(s), f(a), if b then t else f fi , p q, islocal(k), destination(l), lnk(k), filter(P;l), x.A(x), a = b, source(l), mlnk(m), M.sends(k,s,v), []
FDL editor aliasesd-machine

origin